\begin{tabbing}
1. $n$ : $\mathbb{Z}$
\\[0ex]2. 0 $<$ $n$
\\[0ex]3. \=$\forall$$m$:$\mathbb{N}$, $f$, $x$:Top.\+
\\[0ex](primrec(($n$ {-} 1)+$m$;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)($x$))
\\[0ex]$\sim$
\\[0ex](primrec($n$ {-} 1;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)(primrec($m$;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)($x$)))
\-\\[0ex]4. $m$ : $\mathbb{N}$
\\[0ex]5. $f$ : Top
\\[0ex]6. $x$ : Top
\\[0ex]$\vdash$  \=(primrec($n$+$m$;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)($x$))\+
\\[0ex]$\sim$
\\[0ex](primrec($n$;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)(primrec($m$;$\lambda$$x$.$x$;$\lambda$$i$,$g$. $f$ o $g$)($x$)))
\-
\end{tabbing}